(** ** Matrix Function *)

Require Export List.
Require Export Matrix.Mat_def.
Require Export Matrix.list_function.

Section Matrix_functions.
Variable A:Set.
Variable Zero:A.
Variable One:A.
Variable f:A->A.
Variable f1:A->A->A.


(* ################################################################# *)
(** * Matrix Mapping Function *)

Section Mat_map.

(** ** Definition of dlist_map and matrix_map' *)
(** These functions help to construct the matrix mapping function. *)

Section dlist_matrix'_map.

(** *** dlist_map *)
(** Perform a function operation on all elements in the two-dimensional
    list and return a two-dimensional list. *)
Fixpoint dlist_map (m:list(list A)) :=
  match m with
  | List.cons l m' => List.cons (list_map A f l) (dlist_map m')
  | List.nil => List.nil
  end.

(** *** matrix_map' *)
(** Perform dlist_map operation on the two-dimensional list in the
    matrix and return a two-dimensional list. *)
Definition matrix_map'{m n:nat} (ma:@Mat A m n) :=
  let m' := mat A m n ma in dlist_map m'.

End dlist_matrix'_map.

(** ** Properties of dlist_map and matrix_map' *)
(** These properties help to construct the matrix mapping function. *)

Section lemma_of_ldlma_map.

(** *** height_dlist_map *)
(** The height of the two-dimensional list does not change after 
    mapping operation. *)
Lemma height_dlist_map: forall m ma , 
  height ma = m -> height (dlist_map ma) = m.
Proof.
  induction m.
  induction ma.
  - simpl. auto.
  - simpl. intros. inversion H.
  - induction ma.
    + simpl. intros. inversion H.
    + simpl. intros. f_equal. apply IHm. inversion H. auto.
Qed.
(*inversion*)


(** *** height_matrix_map *)
(** The height of the two-dimensional list in the matrix does not 
    change after mapping operation. *)
Lemma height_matrix_map :  forall {m n:nat} (ma:@Mat A m n), 
  height (matrix_map' ma) = m.
Proof.
  intros.
  induction ma.
  unfold matrix_map'.
  simpl.
  apply height_dlist_map.
  auto.
Qed.

(** *** length_list_map *)
(** The length of the list does not change after mapping. *)
Lemma length_list_map : forall a n , 
  length a = n -> length (list_map A f a) = n.
Proof.
  induction a.
  induction n.
  - simpl. auto.
  - simpl. auto.
  - induction n.
    + simpl. intros. inversion H.
    + simpl. intros. f_equal. apply IHa. auto.
Qed.

(** *** width_dlist_map*)
(** The width of the two-dimensional list does not change after the
    mapping operation. *)
Lemma width_dlist_map: forall n ma,
   width ma n -> width (dlist_map ma) n.
Proof.
  induction n. induction ma.
  - simpl. auto.
  - simpl. intros. split. induction a. simpl. auto. 
    inversion H. inversion H0. apply IHma. apply H.
  - induction ma.
    + simpl. auto.
    + simpl. intros. split. apply length_list_map. apply H. apply IHma. apply H.
Qed.

(** *** width_dlist_map*)
(** The width of the two-dimensional table generated by the mapping of
    the m×n size matrix is n *)
Lemma width_matrix_map: forall {m n:nat} (ma:@Mat A m n), 
  width (matrix_map' ma) n.
Proof.
  intros.
  induction ma.
  unfold matrix_map'.
  simpl.
  apply width_dlist_map.
  auto.
Qed.

Lemma list_map_app: forall a b,
  list_map A f (a ++ b) = list_map A f a ++ list_map A f b.
Proof.
  induction a. simpl. auto.
  intros. simpl. f_equal. apply IHa.
Qed.

Lemma dlist_map_app: forall a b,
  dlist_map (a ++ b) = dlist_map a ++ dlist_map b.
Proof.   
  induction a.
  - simpl. auto.
  - intros. simpl. f_equal. apply IHa.
Qed. 

Lemma dlist_map_nil_list: forall m,
  dlist_map (nil_list A m) = nil_list A m.
Proof.
  induction m. simpl. auto.
  simpl. f_equal.  apply IHm.
Qed.

End lemma_of_ldlma_map.

(** ** matrix_map *)
(** Matrix Mapping Function *)

Definition matrix_map {m n :nat}(ma:@Mat A m n):=
  let ans := matrix_map' ma in
    mkMat A m n ans (height_matrix_map ma) (width_matrix_map ma).

End Mat_map.

(** * Matrix Operation Function  *)

(** Function for Processing Two Matrices to Perform Some Kind of
    Operation. *)

Section Mat_operf_def.

(** ** Functions for processing two-dimensional list and matrix *)
(** The following two functions are to help define the Matrix 
    Operation Function. *)

Section operf_def.


Print list_each.
(*对l1和l2中的每个元素，分别进行f作用*)
(** *** mat_each' *)
(** This function performs some kind of arithmetic operation on two
    two-dimensional lists. *)
Fixpoint mat_each' (left:list(list A)) (right:list(list A)) :=
  match left ,right with
  | a::o,b::p => list_each A f1 a b :: mat_each' o p
  | _ , _ => nil
  end.
(*带有'的函数，都是对二维表的操作*)

(** *** mat_each *)
(** This function performs some kind of arithmetic operation on two
    matrix. *)
Definition mat_each {m n:nat}(left:@Mat A m n) (right:@Mat A m n) :=
  let l := mat A m n left in
  let r := mat A m n right in
    mat_each' l r.

End operf_def.

(** ** Properties of The Functions Above *)
(** These properties help to define the Matrix Operation Function. *)

Section operf_lemma.

(** *** height_mat_each' *)
(** The operation of two two-dimensional lists with the same height
    results in the same height of the two-dimensional list. *)
Lemma height_mat_each': forall m (left right:list (list A)), 
  height left = m -> height right = m -> 
  height (mat_each' left right) = m.
Proof.
  induction m.
  induction left.
  induction right.
  - simpl. auto.
  - simpl. auto.
  - intros. inversion H.
  - induction left. induction right.
    + simpl. intros. inversion H.
    + simpl. intros. inversion H.
    + induction right.
      { simpl. intros. inversion H0. }
      { simpl. intros. 
        apply eq_S. apply IHm. auto. auto. }
Qed.

(** *** height_mat_each *)
(** Two matrix operations with the same height get the height of the
    two-dimensional list unchanged. *)
Lemma height_mat_each : forall
  {m n:nat} (left right :@Mat A m n),
  length (mat_each left right) = m.
Proof.
  intros.
  unfold mat_each.
  apply height_mat_each'.
  apply (mat_height A m n left).
  apply (mat_height A m n right).
Qed.

(** *** width_mat_each' *)
(** The operation of two two-dimensional lists with the same width
    results in the same width of the two-dimensional list. *)
Lemma width_mat_each': forall n (left right:list(list A)) ,
  width left n -> width right n -> 
  width (mat_each' left right) n.
Proof.
  induction n.
  induction left.
  induction right.
  - simpl. auto.
  - simpl. auto.
  - intros. simpl. destruct right. auto. rewrite <- list_app. simpl. 
    apply  width_cons in H. apply width_cons in H0. destruct H. 
    apply length_zero_iff_nil in H.  rewrite H. simpl. auto. 
    split. auto. apply IHleft. auto. apply H0. 
  - induction left. induction right.
    + simpl. auto.
    + simpl. auto.
    + induction right.
      { simpl. auto. }
      { simpl. intros. split. apply list_each_length.
        destruct H. auto. destruct H0. auto. apply IHleft. 
        destruct H. auto. destruct H0. auto. }
Qed.

(** *** width_mat_each *)
(** Two matrix operations with the same width get the width of the
    two-dimensional list unchanged. *)
Lemma width_mat_each : forall{m n:nat} 
  (left right : @Mat A m n), 
  width (mat_each left right) n.
Proof.
  intros.
  unfold mat_each.
  apply width_mat_each'.
  apply (mat_width A m n left).
  apply (mat_width A m n right).
Qed.

(** *** mat_each'_cons *)
Lemma mat_each'_cons : forall (a b:list A)
  (ma mb: list (list A)), 
  mat_each' (a::ma) (b::mb) = (list_each A f1 a b)::(mat_each' ma mb).
Proof.
  induction a.
  - intros. simpl. f_equal.
  - induction b.
    + intros. simpl. f_equal.
    + intros. simpl. f_equal.
Qed.

Lemma mat_each'_app: forall (ma mb mc md:list(list A)),
  height ma = height mc -> height mb = height md->
  mat_each' (ma++ mb) (mc++md) 
  = (mat_each' ma mc)++(mat_each' mb md).
Proof.
  induction ma. induction mb.
  simpl. auto. induction mc. induction md.
  auto. intros. simpl. auto. intros. inversion H.
  induction mb. induction mc. intros. inversion H.
  induction md. intros. simpl. f_equal. apply IHma.
  inversion H. auto. auto. intros. inversion H0.
  induction mc. intros. inversion H. intros. induction md.
  intros. inversion H0. simpl. f_equal. apply IHma.
  inversion H. auto. apply H0.
Qed.

Lemma mat_each'_nil_list_l:forall m ma,
  height ma = m ->
  mat_each' (nil_list A m) ma = nil_list A m .
Proof.
  induction m.
  induction ma.
  simpl. auto. intros. inversion H. induction ma.
  intros. inversion H. intros. simpl.
  f_equal. apply IHm. inversion H. auto. 
Qed.

Lemma mat_each'_tail:forall m (ma mb: list(list A)),
  height ma = m -> height mb = m ->
  tl (mat_each' ma mb) 
  = mat_each'(tl  ma) (tl  mb).
Proof.
  induction m.
  induction ma. induction mb. auto. intros. inversion H0.
  intros. inversion H. induction ma. intros. inversion H.
  induction mb. intros. inversion H0. intros.
  simpl. auto.
Qed.
 

End operf_lemma.

(** ** matrix_each *)
(** This function performs some arithmetic operation on the 
    corresponding elements in the two matrices and returns the matrix. *)
Definition matrix_each{m n:nat}(left right:@Mat A m n):=
  let ans := mat_each left right in
    mkMat A m n ans 
   (height_mat_each left right) (width_mat_each left right).

End Mat_operf_def.

End Matrix_functions.